(*
 * Copyright (c) 2009, Palle Raabjerg
 * All rights reserved.
 *
 * Redistribution and use in source and binary forms, with or without
 * modification, are permitted provided that the following conditions are met:
 *
 *   * Redistributions of source code must retain the above copyright notice,
 *     this list of conditions and the following disclaimer.
 *   * Redistributions in binary form must reproduce the above copyright notice,
 *     this list of conditions and the following disclaimer in the documentation
 *     and/or other materials provided with the distribution.
 *
 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
 * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
 * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
 * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE
 * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR
 * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
 * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
 * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
 * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
 * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
 * POSSIBILITY OF SUCH DAMAGE.
 *)
(** The Aconv module traverses the syntax tree of Spi calculus elements, and performs alpha conversion.
    Alpha converting a spi process to avoid name clashes makes capture-avoiding substitution a trivial operation.
*)

open Spitree;;

(** SMap is the basis for the substitution map of the
    alpha conversion function. The substitution map
    indicates what each name in the current scope must
    be substituted with.
*)
module SMap = Map.Make(String)

(** Called on free names.
    If the name exists in the substitution map, the name is substituted according to the map.
    If the name does not exist in the substitution map, a new unique name is generated, and the map and accumulator is updated.
    @param x Free name
    @param accum Accumulator
    @param substMap Substitution map

    @return A tuple containing the new name, and the updated accumulator and substitution map.

*)
let subst_name x accum substMap =
  if SMap.mem x substMap then
    (SMap.find x substMap, accum, substMap)
  else
    let newname = (string_of_int accum) ^ "_" ^ x in
    let newMap = SMap.add x newname substMap in
    (newname, accum + 1, newMap)

(** Called on the binding occurrences of names. A new unique name is generated, and the map and accumulator is updated. To preserve scope, a previous mapping of the name is returned for reinsertion when the scope is exited.
    @param x Binding name
    @param accum Accumulator
    @param substMap Substitution map

    @return A tuple containing the new name, the updated accumulator, the substitution map, and the previous mapping of the name.
*)
let bind x accum substMap =
  let newname = (string_of_int accum) ^ "_" ^ x in
  let newMap = SMap.add x newname substMap in
  if SMap.mem x substMap then
    let oldname = SMap.find x substMap in
    (newname, accum + 1, newMap, (x, oldname))
  else
    (newname, accum + 1, newMap, (x, ""))

(** Called when exiting the scope of a bound name. The mapping for that name is replaced by the stored mapping for the outer scope.
    @param x Bound name
    @param oldname Previously stored mapping of the outer scope
    @param substMap Substitution map

    @return The new substitution map
*)
let unbind (x, oldname) substMap =
  if oldname = "" then
    SMap.remove x substMap
  else
    SMap.add x oldname substMap

(** Alpha conversion of messages
    @param msg Syntax tree of message
    @param a Accumulator
    @param s Substitution map

    @return Updated message, accumulator and substitution map
*)
let rec msg_subst msg a s = match msg with
  | Name (x) ->
      let (x_dat, ua, us) = (subst_name x a s) in
      (Name (x_dat), ua, us)
  | Encr (m, n) ->
      let (m_dat, ua, us) = (msg_subst m a s) in
      let (n_dat, ua, us) = (msg_subst n ua us) in
      (Encr (m_dat, n_dat), ua, us)
  | MPair (m, n) ->
      let (m_dat, ua, us) = (msg_subst m a s) in
      let (n_dat, ua, us) = (msg_subst n ua us) in
      (MPair (m_dat, n_dat), ua, us)
  | Ok -> (Ok, a, s);;

(** Alpha conversion of effects
    @param msg Syntax tree of effect
    @param a Accumulator
    @param s Substitution map

    @return Updated effect, accumulator and substitution map
*)
let rec reso_subst reso a s = match reso with
  | Reso (l, m) ->
      let (m_dat, ua, us) = (msg_subst m a s) in
      (Reso (l, m_dat), ua, us)
  | RPair (r, t) ->
      let (r_dat, ua, us) = (reso_subst r a s) in
      let (t_dat, ua, us) = (reso_subst t ua us) in
      (RPair (r_dat, t_dat), ua, us)
  | Empty -> (Empty, a, s);;

(*let literal_subst (pred, termlist) a s =
  let (subst_termlist, ua, us) =
    List.fold_right (fun term (data_accum, ua, us) ->
		       match term with
			 | Var(x) -> (term::data_accum, ua, us)
			 | SpiMsg(m) ->
			     let (term_dat, ua, us) = (msg_subst m ua us) in
			       (SpiMsg(term_dat)::data_accum, ua, us)
		    ) termlist ([], a, s)
  in
    ((pred, subst_termlist), ua, us);;

let hclause_subst clause a s =
  List.fold_right (fun literal (data_accum, ua, us) ->
		     let (lit_dat, ua, us) = (literal_subst literal ua us) in
		       (lit_dat::data_accum, ua, us)
		  ) clause ([], a, s);;

let datalog_subst data a s =
  List.fold_right (fun clause (data_accum, ua, us) ->
		     let (cl_dat, ua, us) = (hclause_subst clause ua us) in
		       (cl_dat::data_accum, ua, us)
		  ) data ([], a, s);;*)

(** Alpha conversion of type
    @param typ Syntax tree of type
    @param a Accumulator
    @param s Substitution map

    @return Updated type, accumulator and substitution map
*)
let rec typ_subst typ a s = match typ with
  | Un -> (Un, a, s)
  | Key (t) ->
      let (t_dat, ua, us) = (typ_subst t a s) in
      (Key (t_dat), ua, us)
  | Ch (t) ->
      let (t_dat, ua, us) = (typ_subst t a s) in
      (Ch (t_dat), ua, us)
  | TPair (x, t, u) ->
      let (t_dat, ua, us) = (typ_subst t a s) in
      let (x_dat, ua, us, binding) = (bind x ua us) in
      let (u_dat, ua, us) = (typ_subst u ua us) in
      (TPair (x_dat, t_dat, u_dat), ua, (unbind binding us))
  | TOk (r) ->
      let (r_dat, ua, us) = (reso_subst r a s) in
      (TOk (r_dat), ua, us)
  | Unknown -> (Unknown, a, s);;

(** Alpha conversion of process
    @param proc Syntax tree of process
    @param a Accumulator
    @param s Substitution map

    @return Updated process, accumulator and substitution map
*)
let rec proc_subst proc a s = match proc with
  | Out (m, n) ->
      let (m_dat, ua, us) = (msg_subst m a s) in
      let (n_dat, ua, us) = (msg_subst n ua us) in
      (Out (m_dat, n_dat), ua, us)
  | In (m, x, p) ->
      let (m_dat, ua, us) = (msg_subst m a s) in
      let (x_dat, ua, us, binding) = (bind x ua us) in
      let (p_dat, ua, us) = (proc_subst p ua us) in
      (In (m_dat, x_dat, p_dat), ua, (unbind binding us))
  | InRepl (m, x, p) ->
      let (m_dat, ua, us) = (msg_subst m a s) in
      let (x_dat, ua, us, binding) = (bind x ua us) in
      let (p_dat, ua, us) = (proc_subst p ua us) in
      (InRepl (m_dat, x_dat, p_dat), ua, (unbind binding us))
  | Nu (x, t, p) ->
      let (t_dat, ua, us) = (typ_subst t a s) in
      let (x_dat, ua, us, binding) = (bind x ua us) in
      let (p_dat, ua, us) = (proc_subst p ua us) in
      (Nu (x_dat, t_dat, p_dat), ua, (unbind binding us))
  | PPara (p, q) ->
      let (p_dat, ua, us) = (proc_subst p a s) in
      let (q_dat, ua, us) = (proc_subst q ua us) in
      (PPara (p_dat, q_dat), ua, us)
  | PNil -> (PNil, a, s)
  | Begin (l, m) ->
      let (m_dat, ua, us) = (msg_subst m a s) in
      (Begin (l, m_dat), ua, us)
  | End (l, m) ->
      let (m_dat, ua, us) = (msg_subst m a s) in
      (End (l, m_dat), ua, us)
  | Decrypt (m, x, t, n, p) ->
      let (m_dat, ua, us) = (msg_subst m a s) in
      let (t_dat, ua, us) = (typ_subst t ua us) in
      let (n_dat, ua, us) = (msg_subst n ua us) in
      let (x_dat, ua, us, binding) = (bind x ua us) in
      let (p_dat, ua, us) = (proc_subst p ua us) in
      (Decrypt (m_dat, x_dat, t_dat, n_dat, p_dat), ua, (unbind binding us))
  | Split (m, x, t, y, u, p) ->
      let (m_dat, ua, us) = (msg_subst m a s) in
      let (t_dat, ua, us) = (typ_subst t ua us) in
      let (x_dat, ua, us, xbinding) = (bind x ua us) in
      let (u_dat, ua, us) = (typ_subst u ua us) in
      let (y_dat, ua, us, ybinding) = (bind y ua us) in
      let (p_dat, ua, us) = (proc_subst p ua us) in
      (Split (m_dat, x_dat, t_dat, y_dat, u_dat, p_dat), ua, (unbind xbinding (unbind ybinding us)))
  | Match (m, t, n, x, usub, p) ->
      let (m_dat, ua, us) = (msg_subst m a s) in
      let (t_dat, ua, us) = (typ_subst t ua us) in
      let (n_dat, ua, us) = (msg_subst n ua us) in
      let (usub_dat, ua, us) = (typ_subst usub ua us) in
      let (x_dat, ua, us, binding) = (bind x ua us) in
      let (p_dat, ua, us) = (proc_subst p ua us) in
      (Match (m_dat, t_dat, n_dat, x_dat, usub_dat, p_dat), ua, (unbind binding us))
(*  | Datprog(d) ->
      let (d_dat, ua, us) = (datalog_subst d a s) in
      (Datprog(d_dat), ua, us)
  | Expect(l) ->
      let (l_dat, ua, us) = (literal_subst l a s) in
      (Expect(l_dat), ua, us)*);;
